#include <stdlib.h>

/*@
  @ requires 0<=n;
  @ ensures \result==0 <==> (\exists integer k, x; (k>=0 && x>=0 && k!=n && k!=1 && x!=n && x!=1 && n==k*x) || n == 0 || n == 1);
  @*/


int prime(int n)
{
  int i;
  int r;
  if(n<2)
      r=0;
  else
    {
      if (n == 2)
	r=1;
      else
	{
	  i=2;
	  /*@ loop invariant ((i+1)*(i+1)<=n) && \forall integer k, x; (k>=2 && x>=2 && k<i && x<i) ==> n!=k*x;
	    @ loop variant n-i*i;
	    @*/
	  while ((i*i<=n) && (n%i != 0))
	    i = i+1;
	  r = (n%i!=0);
	}
    }
  return r;
}
